package bcontractor.propositional.minisat;

import java.io.IOException;
import java.io.InputStream;
import java.util.Iterator;

import bcontractor.api.SentenceSet;
import bcontractor.propositional.PropositionalSentence;

/**
 * Prepares a propositional sentence set as input to a MiniSat solver.
 * 
 * @author lundberg
 * 
 */
public class MiniSatInput extends InputStream {

	private final Iterator<PropositionalSentence> sentences;

	private String buffer;

	private int pos = 0;

	/**
	 * Construtor
	 * 
	 * @param problem
	 *            problem
	 */
	public MiniSatInput(SentenceSet<PropositionalSentence> sentences) {
		int variables = 0;
		int clauses = 0;
		for (PropositionalSentence sentence : sentences) {
			variables = Math.max(variables, sentence.getMaxvar());
			clauses += sentence.getClauses().length;
		}
		this.buffer = String.format("p cnf %s %s", variables, clauses);
		this.sentences = sentences.iterator();
	}

	/**
	 * {@inheritDoc}
	 */
	@Override
	public int read() throws IOException {
		if (this.pos < this.buffer.length()) {
			return this.buffer.charAt(this.pos++);
		} else if (this.sentences.hasNext()) {
			this.buffer = this.nextSentence();
			this.pos = 1;
			return this.buffer.charAt(0);
		} else {
			return -1;
		}
	}

	/**
	 * 
	 * @return next clause
	 */
	private String nextSentence() {
		StringBuilder builder = new StringBuilder();
		for (int[] clause : this.sentences.next().getClauses()) {
			for (Integer literal : clause) {
				builder.append(" " + literal);
			}
			builder.append(" 0");
		}
		return builder.toString();
	}
}
